\begin{tabbing} 1. \=$\forall$$n$, $a$, $b$:$\mathbb{N}$.\+ \\[0ex]\{\=$m$:$\mathbb{N}\mid$ \+ \\[0ex]$\forall$$k$:$\mathbb{N}$. \\[0ex]($a$ = fib($k$)) \\[0ex]$\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ ($b$ = 0)) \\[0ex]$\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ ($b$ = fib($k$ {-} 1))) \\[0ex]$\Rightarrow$ ($m$ = fib($n$+$k$))\} \-\-\\[0ex]$\vdash$ $\forall$$n$:$\mathbb{N}$. \{$m$:$\mathbb{N}\mid$ $m$ = fib($n$)\} \end{tabbing}